$\forall$$A$:Type, $P$:(($A$ List)$\rightarrow$Prop). strong\_safety($A$;$x$.$P$($x$)) $\in$ Prop